<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Issue2623</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\pagestyle{empty}

\begin{document}

\noindent Text.
\AgdaHide{
</a><a id="109" class="Markup">\begin{code}</a>
  <a id="124" class="Keyword">mutual</a>
<a id="131" class="Markup">\end{code}</a><a id="141" class="Background">}
</a><a id="143" class="Markup">\begin{code}</a>
    <a id="160" class="Keyword">postulate</a> <a id="A"></a><a id="170" href="Issue2623.html#170" class="Postulate">A</a> <a id="172" class="Symbol">:</a> <a id="174" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="178" class="Markup">\end{code}</a><a id="188" class="Background">
More text.
\begin{AgdaMultiCode}
</a><a id="222" class="Markup">\begin{code}</a>
  <a id="237" class="Keyword">mutual</a>
<a id="244" class="Markup">\end{code}</a><a id="254" class="Background">
</a><a id="255" class="Markup">\begin{code}</a>
    <a id="272" class="Keyword">postulate</a> <a id="B"></a><a id="282" href="Issue2623.html#282" class="Postulate">B</a> <a id="284" class="Symbol">:</a> <a id="286" href="Agda.Primitive.html#311" class="Primitive">Set</a>
<a id="290" class="Markup">\end{code}</a><a id="300" class="Background">
\end{AgdaMultiCode}
Even more text.

\end{document}</a></pre></body></html>